Lambda the Ultimate

A couple of small items that caught my attention.

• Fritz Kunze (President of Franz Inc.) reveals the secrets to successful programming language business.
• An interview about reddit which includes the ultimate question: Why Lisp?
• Tim Bray on abstracting the Web using continuations (well, sort of).

Lock -Free Data Structures using STMs in Haskell. Anthony Discolo, Tim Harris, Simon Marlow, Simon Peyton Jones, and Satnam Singh. Submitted to FLOPS'06.

This paper explores the feasibility of re-expressing concurrent algorithms with explicit locks in terms of lock free code written using Haskell's implementation of Software Transactional Memory (STM). Preliminary experimental results are presented which show that for multi-processor systems the simpler lock free implementations offer competitive or superior performance when compared to their corresponding the lock based implementations.

The ArrayBlockingQueue class from JSR-166 is the basis for this experiment. A selection of representative methods from the three interfaces supported by this class is reimplemented in Haskell. Two implementations are provided: one using mutexes and semaphores from the IO monad and one based on STMs.

The performance of the two versions is compared and discussed.

John Vlissides, of GoF fame, passed away on Thursday, November 24, 2005, after a lengthy illness.

More on John on the wiki page dedicated to his memory.

Systematic search for lambda expressions by Susumu Katayama

This paper presents a system for searching for desired small functional programs by just generating a sequence of type-correct programs in a systematic and exhaustive manner and evaluating them. The main goal of this line of research is to ease functional programming, along with the subgoal to provide an axis to evaluate heuristic approaches to program synthesis such as genetic programming by telling the best performance possible by exhaustive search algorithms. While our previous approach to that goal used combinatory expressions in order to simplify the synthesis process, which led to redundant combinator expressions with complex types, this time we use de Bruijn lambda expressions and enjoy improved results.

Although the algorithm is slow and only works on small expressions, it looks helpful. Perhaps there could be some synthesis with Hoogλe, or whatever the name is after Google makes them change it.

Due to recent discussions here on LtU and on the Haskell mailing lists I've compiled a list of links to implementations of monads in various languages. If you know of any that aren't listed here, please submit them in a comment.

• Clean
• Haskell
• Java
• Joy
• OCaml
• Perl
• Prolog
• Python
• Ruby
• Scheme

A longer article with side by side comparisons of the implementations would be interesting, and may help students understand monads by separating them from any one syntax or implementation.

After some hesitation I decided to add a Ruby department to the spotlight category. This is where (home page) posts relating to Ruby should now be filed.

This doesn't imply we now have a special preference for Ruby. It simply reflects that more and more items related to Ruby are posted, and I want them easily found. The other language in the spotlight category is Python, which is there for a long time since there were many interesting experiments with Python, which we discussed many times in the past.

Generalized Algebraic Data Types and Object-Oriented Programming. Andrew Kennedy and Claudio Russo. OOPSLA, October 2005, San Diego, California.

Generalized algebraic data types (GADTs) have received much attention recently in the functional programming community. They generalize the type-parameterized datatypes of ML and Haskell by permitting constructors to produce different type-instantiations of the same datatype. GADTs have a number of applications, including strongly-typed evaluators, generic pretty-printing, generic traversals and queries, and typed LR parsing. We show that existing object-oriented programming languages such as Java and C# can express GADT definitions, and a large class of GADT-manipulating programs, through the use of generics, subclassing, and virtual dispatch. However, some programs can be written only through the use of redundant run-time casts. We propose a generalization of the type constraint mechanisms of C# and Java to avoid the need for such casts, present a Visitor pattern for GADTs, and describe a switch construct as an alternative to virtual dispatch on datatypes. We formalize both extensions and prove a type soundness result.

I've been waiting for awhile for this paper to be available online.

This paper is, of course, related to the other items posted here about GADTs. The examples in the introduction might be somewhat relevant to the recent discussion about the static versus dynamic features of Java, and its type system.

Simon Peyton Jones has a new paper about type inferencing and GADT's: Simple unification-based type inference for GADTs

Generalized algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. Our contribution is to show how to exploit programmer-supplied type annotations to make the type inference task almost embarrassingly easy. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

This paper is a much simplified and completely-rewritten version of his earlier paper Wobbly types: type inference for generalised algebraic data types

LtU readers know that I am long time advocate of code reading. As I've argued here in the past, reading great code is the best way to acquire good programming skills. It's also a pleasure to read good code. Yes - reading code can be fun.

It turns out that I am not alone (though my conception of a code reading workshop is perhaps somewhat different than the things discussed there).

Anyway, this is a chance to continue one of my pet memes. Many of the pieces of great code I've read over the years come from language processing tools (e.g., compilers, meta-programming systems etc.) I don't think this is a coincidence.

Now's your chance to tell us your favorite examples.

The rules: The code must be beautiful and it must be programming language related (and no, being written in a programming language isn't enough).

In the beginning was game semantics

Giorgi Japaridze

[...] the story and philosophy of computability logic (CL) [...]
According to its philosophy, syntax — the study of axiomatizations or any other, deductive or nondeductive string-manipulation systems — exclusively owes its right on existence to semantics, and is thus secondary to it. CL believes that logic is meant to be the most basic, general-purpose formal tool potentially usable by intelligent agents in successfully navigating real life. And it is semantics that establishes that ultimate real-life meaning of logic. Syntax is important, yet it is so not in its own right but only as much as it serves a meaningful semantics, allowing us to realize the potential of that semantics in some systematic and perhaps convenient or efficient way.
[...]
the philosophy of CL relies on two beliefs that, together, present what can be considered an interactive version of the Church-Turing thesis:

Belief 1.

The concept of static games is an adequate formal counterpart of our intuition of ("pure", speed-independent) interactive computational problems.

Belief 2.

The concept of winnability is an adequate formal counterpart of our intuition of algorithmic solvability of such problems.

I already posted links to papers of Giorgi Japaridze several times, but most of them were pretty technical, and also that was before the latest expansion of LtU's readership.

In short, CL is about trying to generalize traditional (both classical and intuitionistic) logic beyond batch computation (well, I hope everybody knows why logic is relevant to computation, if not - look for Curry-Howard isomorphism, or CHI). There are several approaches to doing that, but Giorgi believes they go the wrong way by trying to build upon the syntax, while it's semantics that is primary.

If you believe that computation is more than calculating a function, and that logic is a good way to understand computation - then I recommend to read at least the introduction and the references' list of this paper (the paper is a single chapter for a book, would love to see the whole book).